引介|形式化验证Gasper共识机制的终局性

Gasper 是一个由信标链协议（即将到来的 以太坊 2.0 网络的底层协议）实现的抽象的权益证明协议层。Gasper 的关键部分就是一套终局性机制（finality mechanism），用于保证交易的持存性（durability）和系统的不间断运作不会被攻击破坏。

我们很高兴宣布， Runtime Verification 和 以太坊基金会 长久合作中的另一大里程碑圆满成功：我们开发了一套形式框架来模拟和验证信标链协议，并成功形式化地证明了 Gasper 终局性的正确性（correctness）；并且，我们还使用这些结果证明了信标链的 Gasper 抽象实现同样具备这些属性。模型和证明脚本都可以在 此处 找到。

在本文中，我们希望介绍这一成就的第一部分：验证 Gasper 的属性。所以，什么是 Gasper？如何能形式化地验证其属性？这种形式化验证有何意义？

Gasper

信标链 协议是一套新的权益证明协议，是以太坊未来的重大升级 “ 以太坊 2.0 ” 的核心。在信标链协议中，参与的节点（或者叫 “验证者”）都在系统中存有保证金（stake，形式为 ETH）。验证者通过向网络提交 “见证消息（attestation）” 来证实区块的有效性并为其多种属性投票。信标链协议本身包含了多种工具，以帮助验证者们对区块链的最新状态达成共识。

Gasper 为信标链协议中的终局性工具（finality gadget）提出了一套抽象但准确的描述，还定义了分叉选择规则；终局性 工具 用于确定哪些区块应被参与者认定为已经确定的、不可更改的，分叉选择规则则用于在链产生分叉时确定哪个分叉是主链。Gasper 中的终局性（finality）一般化了始创于《 Casper Friendly Finality Gadget (Casper FFG) 》论文中的概念，让 “终局化（finalization）” 获得了更通用的形式。

合理化与终局化（Justification and Finalization）

终局性概念仅与 “检查点区块” （也叫 “时段边界区块”，就是位于时段（epoch）起点处的区块）有关。见证消息中有一部分叫 “合理化投票” ，验证者在合理化投票中将一个来源检查点区块（source checkpoint block）和稍后的一个目标检查点区块（target checkpoint block）关联起来，直观地表明发起该见证消息的验证者认为 “我们可以从来源检查点的状态移动到目标检查点的状态”。实际上，一份合理化投票表明了：（1）发起投票的验证者；（2）来源检查点及其合理化高度（justification height）；（3）目标检查点及其合理化高度（justification height）。

当且仅当条件满足：（1）来源检查点 B0 已得到合理化；（2）大多数人（即至少 2/3 的验证者）同样投票给 B0-B1 来源-目标对；则目标检查点 B1 就经由来源检查点 B0 得到了合理化。

当且仅当大多数验证者将 B0 与其 K 代子孙检查点 Bk 关联起来，则 B0 获得 K 阶终局性（k > 0），且 B0 与 Bk 之间的所有检查点都被终局化。注意，创世区块本身被认为既已得到合理化，又有终局性。下图演示了 Gasper 中的合理化和终局化概念。

罚没条件（Slashing Conditions）

如果验证者尝试偏离协议要求、提交自相矛盾的投票，则该验证者会被惩罚：其保证金会被扣除一大部分。Gasper 定义了两个条件（也称罚没条件）来定义何谓自相矛盾的投票：

1. 双重投票（Double-voting）：验证者发布了两个截然不同的投票，但两个投票的目标高度是同一个高度。
2. 环绕投票（Surround-voting）：验证者发布的一个投票所关联的两个检查点恰好在自己所发布的另一个投票的两个检查点高度范围内。

发起双重投票的验证者被认为违反了第一罚没条件；而发起环绕投票的验证者则违反了第二罚没条件。不论是哪种情况，违反规则的验证者都会被扣除大量保证金。

正确性（Correctness Properties）

与其它拜占庭容错型（Byzantine Fault Tolerance，BFT）协议相同，Gasper 协议的一个关键底层假设是绝大多数验证者（超过 2/3，以保证金数量定义）是诚实的、会遵循协议的要求。在此假设下，Gasper 有两大基本属性：

• 可追责的安全性 （Accountable Safety）：不会有两个属于不同分叉的区块都被终局化，除非有至少 1/3 的验证者（以保证金数量计）被罚没；
• 似然活性 （Plausible Liveness）：无论区块链过往发生了什么事，区块的终局化进程永远不会陷入僵局。

此外，在验证者集合会动态变化的环境（因为验证者会离开网络，也会有新验证者加入，活跃验证者集合可能会发生改变）中，第三种属性量化了在有人违反协议规则时可被罚没的保证金体量：

• 可罚没下限 （Slashable bound）：只要能够使用协议外条件来控制验证者的激活和退出参数条件，就能证明（在打破安全性时）可被罚没的保证金数量有一个下限。

动态验证者集合（也即信标链协议所实现的）引入了另一个有挑战性的问题：系统不再那么能够可靠地惩罚恶意验证者，因为他们可能会在作恶之后、保证金被实际罚没之前离开网络。而可罚没下限属性使得调整活跃验证者集合的可变幅度、维持最低水平的可追责性成为可能。

验证 Gasper 的终局性

Gasper 旨在为终局性提供一个数学化的、精确的、可用来形式化地证明其正确性的描述；这种正确性也是证明信标链协议安全性的关键。以太坊平台正日渐被用作大型金融交易系统的股价，更突出了安全性保证的前所未有的重要性。

与以太坊基金会通力合作，我们已经使用 Coq 证明助手，形式化了 Gasper 在动态验证者集合一般条件下的终局性机制。我们在这一条件下指出并证明了 Gasper 的所有三种关键属性：可追责的安全性、似然活性以及可罚没下限；所有证明都使用了同一个 Coq 模型。

对协议的演绎论证给了我们对相关主张正确性和安全性的极大信心，因为演绎论证保证没有未经指明的假设，也没有无效的演绎推理步骤。它也明确了为使论点成立所需的所有假设。形式化过程也能反哺协议的描述，使协议的描述能更准确、更完整。

这里我们仅对这一成就给出概要的说明。完整的细节可见：

1. 该项目的技术报告
2. 该项目的 Github 代码库

建模及验证方法

第一步是开发一个协议的模型，让我们能够表达出所有我们希望形式化地指出并证明的关键属性。这个模型建立在我们之前验证 Casper FFG 的安全性和活性的 工作 基础上（此前的模型已经定义了 Gasper 终局性机制的早期版本）。

这一模型有三个主要的结构化模块：

验证者和团体（Validators and quorums）。验证者被抽象地表示为一个有限型（finite type）的成员（成员数量有限，而且可以枚举），写为 Validator : finType 。每个验证者都有一份保证金；这一事实我们建模成一个未解释的函数 stake : {fmap Validator -> nat} ，保存验证者与其保证金数量（一个自然数）的映射。此外，给定一个验证者集合，其权重 wt 定义为该集合中所有验证者保证金数量的总和：

\sum 是求和运算符； stake.[st_fun v] 则给出了相应于验证者 v 的保证金数量（ st_fun 即假设每个验证者都必须在系统中有一份保证金）。

wt 函数的几个属性源自其定义，例如：空验证者集的权重必然为 0，两个互不相交的集合的合集的权重就是各自权重的和。这些属性在涉及可罚没下限属性中关于权重的推理时会派上用场。

此外，因为我们要模拟动态的验证者集合，也就是活跃验证者的集合可能会随区块发生改变，我们声明了一个抽象的（有限）映射 vset : {fmap Hash -> {set Validator}} ，给出一个区块处的活跃验证者集合。现在，使用 vset 和 wt ，我们就能定义什么是绝对多数集合：

在某个区块处，如果活跃验证者集合的一个子集的权重超过整个集合权重的 2/3，则该子集就是一个绝对多数集合。

区块树。我们用区块哈希的有限型来模拟一个区块 Hash:finType ，另外，用 genesis 代表创世区块。我们使用符号 h1 <~ h2 这样的符号来表示区块父子关系（ h1 就是 h2 的父辈），以此模拟检查点区块树。

接下来我们使用 h1 <~* h2 来定义祖先关系， h1 就是 h2 的祖先，而 h2 就是 h1 的后代（h1 和 h2 可以是同一个区块）。至于祖先关系的属性，比如祖先的祖先也是祖先，与父子关系的属性类同。

全局状态。状态可表示为由合理化投票组成的有限集合，投票的形式是 (v, s, t, s_h, t_h) ，而 v 是发起投票的验证者， s 和 t 是 TA 支持的来源区块和目标区块，而 s_h 和 t_h 是它们的见证高度（attestation height）。某一个投票是否有人发起过可通过一个布尔成员断言确定：

实例规范

基于这些定义以及它们相应的属性，我们定义出了模型中的所有其它结构和属性，包括罚没条件、团体交集属性（quorum intersection property），还有合理化以及终局化。举例而言，在一次违反协议的事件中，罚没某个团体的属性可使用如下的抽象成员约束而得到定义：

该命题指出，罚没一个团体意味着，在某些区块 bL 和 bR 处存在着两个绝对多数团体 vL 和 vR ，这两个团体的交集就是被罚没验证者（发起了双重投票或者环绕投票）的完整集合。注意，在活跃验证者集合一直固定的特殊条件下，这些绝对多数集合的交集的权重至少是所有保证金的 1/3。

另一个例子是一个终局化分叉（即违反安全性的情形）的定义：

该命题指出两个相互矛盾的区块 b1 和 b2 都被终局化了（因为 b1 和 b2 都不是对方的祖先区块）。这两个区块可以是在任意合理化高度的时候被任意长的链终局化的。

这些定义和结果组中被用来指出和证明可追责的安全性、似然活性以及可罚没下限三种定理。为清楚起见，我们还用下式重新定义了可追责安全性定理的表述：

这个定义很简单，只是说：如果安全性被打破（出现了任何被敲定的分叉），那必定意味着某个验证者集合会被罚没。这个证明机械化了 Gasper 给出的非正式论证，并展示了为什么分叉获得终局化就意味一定有两个绝对多数团体违反了其中一条罚没条件，因此其交集可被罚没。

我们的技术报告描述了形式化过程以及这些属性的证明，而我们的项目代码库提供了完整的详述。

继续前进

在本文中，我们讲解了 Runtime Verification 与以太坊基金会合作成就的第一部分。这第一部分乃是（在验证者集合会动态变化的条件下）形式化 Gasper 并证明其关键的三种属性：可追责的安全性、似然活性以及可罚没下限。我们成就的第二部分，在本文中还未涉及的，是展示如何将这些结果代入更加精细的模型（用 K 框架 写就）中，给出一个信标链状态转换函数的抽象版本。我们后面会用另一篇文章来展示这一成果。

完成这个里程碑还意味着我们向这场合作的终极目标（形式化地证明信标链协议满足所有三种关键属性、并能清楚地声明一个非常接近于协议详述的抽象版本所需的所有假设）迈出了重要的一步。

我们期待在这项工作上与以太坊基金会继续合作。在这次接触中，我们对以太坊基金会的几位专家深为感激：Danny Ryan、Carl Beekhuizen、Martin Lundfall、Yan Zhang 以及 Aditya Asgaonkar。

（完）

原文链接: https://runtimeverification.com/blog/formally-verifying-finality-in-gasper-the-core-of-the-beacon-chain/

作者:Musab Alturki

翻译:阿剑